Nuprl Lemma : gcd_reduce_wf
11,40
postcript
pdf
p
,
q
:
. gcd_reduce(
p
;
q
)
(
:
(
:
))
latex
Definitions
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
spreadn(
a
;
w
,
x
,
y
,
z
.
t
(
w
;
x
;
y
;
z
))
,
gcd_reduce(
p
;
q
)
,
t
T
,
x
:
A
.
B
(
x
)
,
Lemmas
nat
wf
origin
p,q:
. gcd_reduce(p; q) 
(:
(: )) p,q:. gcd_reduce(p; q) (: (: )) 
Q
Q
x:A. B(x) Tx:A. B(x)